\begin{tabbing}
msg{-}spec{-}loc{-}decl(${\it snd}$; $i$; ${\it da}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=$\forall$$k$:Knd, $l$:IdLnk.\+
\\[0ex]($\uparrow$fpf{-}dom(product{-}deq(Knd; IdLnk; Kind{-}deq; idlnk{-}deq); $<$$k$, $l$$>$; ${\it snd}$))
\\[0ex]$\Rightarrow$ \=((source($l$) = $i$)\+
\\[0ex]$\wedge$ l\_all(\=map(\=($\lambda$$p$.$p$.1);\+\+
\\[0ex]fpf{-}ap(${\it snd}$; product{-}deq(Knd; IdLnk; Kind{-}deq; idlnk{-}deq); $<$$k$, $l$$>$));
\-\\[0ex]Id;
\\[0ex]${\it tg}$.($\uparrow$fpf{-}dom(Kind{-}deq; rcv($l$,${\it tg}$); ${\it da}$))))
\-\-\-
\end{tabbing}